\relax 
\citation{ec7}
\citation{jh2}
\citation{ba6}
\citation{sca9}
\@writefile{toc}{\contentsline {title}{Formal Specification and Verification of a Narrow Bandwidth Protocol in PVS}{1}}
\@writefile{toc}{\authcount {1}}
\@writefile{toc}{\contentsline {author}{Hai Wan}{1}}
\@writefile{toc}{\contentsline {section}{\numberline {1}Introduction}{1}}
\citation{ds1}
\citation{pvs8}
\@writefile{toc}{\contentsline {section}{\numberline {2}The Narrow Bandwidth Protocol}{2}}
\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces The architecture of the system}}{3}}
\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces ENBCP and LMSP}}{3}}
\@writefile{lof}{\contentsline {figure}{\numberline {3}{\ignorespaces The pseudo-code of ENBCP}}{5}}
\@writefile{lof}{\contentsline {figure}{\numberline {4}{\ignorespaces The state transition graph}}{6}}
\@writefile{lof}{\contentsline {figure}{\numberline {5}{\ignorespaces A typical execution of ENBCP}}{6}}
\@writefile{toc}{\contentsline {section}{\numberline {3} Modeling Protocol Primitives}{7}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.1}Formalizing Time}{7}}
\@writefile{toc}{\contentsline {subsection}{\numberline {3.2}Formalizing Message Deliver Services}{7}}
\@writefile{toc}{\contentsline {section}{\numberline {4}Formalizing the Narrow Bandwidth Protocol in PVS}{9}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.1} Formalizing State Transitions}{9}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.2}Formalizing Timeout}{10}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.3}Formalizing the Communicating Counterpart}{10}}
\@writefile{toc}{\contentsline {subsection}{\numberline {4.4}Formalizing Transfer Events}{11}}
\@writefile{toc}{\contentsline {section}{\numberline {5}Mechanically Proved Properties}{12}}
\@writefile{lof}{\contentsline {figure}{\numberline {6}{\ignorespaces The theorem BeforeSendingExist}}{13}}
\bibcite{ds1}{1}
\bibcite{jh2}{2}
\@writefile{lof}{\contentsline {figure}{\numberline {7}{\ignorespaces  Proof of FinalTheorem\_2}}{14}}
\@writefile{toc}{\contentsline {section}{\numberline {6}Conclusions}{14}}
\bibcite{vr3}{3}
\bibcite{dv4}{4}
\bibcite{dc5}{5}
\bibcite{ba6}{6}
\bibcite{ec7}{7}
\bibcite{pvs8}{8}
\bibcite{sca9}{9}
